COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\magnify{1100}
C00016 ENDMK
C⊗;
2s7∞;;'≠OYEEAπp4*s&+~sc≡['CnfCO/'β;CQβεcWMOπ!β7'w+MSC'p4*s≡C∂?∪.βquE_h*s∪.3q
GgZs#␈Cns'"→Fq?wp4*s≡C∂?∪.YuE_h*s∪.0[nsF∪?aβ&y↓K↔o[{x4Uc∪↔~dJ≠nsnS#?πZs→εK≠{xhRs∪↔5bR"⊗wZs7π&CK↔3]c→β&C↔;{ph*s∪.2r⊗2≤+ns7∂##K↔gZs→ε+3O↔wp4*s&+~rεt#ns7∂##K↔gZs→ε;∪{ph*s∪.2r>K]c7πSG∪↔3nf∪→β?↔sx4*f#↔~rtzSnsnS#?πZs→εs?S{ph*s∪.2r;nfkπS#␈βns2β;{xhRs∪↔5bSnsF∪?cng#QαSwp4*s&+~r:Lcns#⊗{cns'!α:&gsx4*f#↔~qwZs7π&C';Zs{x4Uc∪↔~dns7∂##?C]c→β∂sx4*f#↔~r'Zs7π&C?Cnf∪→β∪wp4*s&+~r⊗∂Zs7π&CK↔3]c→β/{x4Uc∪↔~d
SnsnS#?πZs→εS{xhRs∪↔5cGW?&)
GnfC?c]cO≠∂}#↔↓9k	AABg#Q
Gwp4*s&+~s3O≠Q
G]c3π;>c∃
Fg∪π;∨f+x4(hRs∂S⊗c';↔]c→α≥→↓IA2i56K.≠WKOO3∃αC⊗{∨Kπnk';≥ε;⊃απ∪?['v;x4*g3O/'α↓ICC h*s∂'∪3';/Z←K'&K;≥απ∪??≠∨p4*s∨#K3'v+n;?6+7↔∩↓I1↓IaKxhRs[O↑KA↓IπβP4(hR¬β;.k↔Iε{→βC.{C3∃εCπ[∃εO/↔"βπ?/!βS#*β≠?KnQβ'rβ←#'≡AβS#/IβO#␈+3⊃β?∪'S∀hSS#↔O⊃βCK}{≠Mβ6{IβSF)β#?n+←?KZβπOON;;7↔w!9↓α&C∃β7∞K9βG.+OS'}qβO↔.kMβSzβ∀4VC?]βo+∂!β&yβOπJaβ%;*q1β←FQβ∂∞qβ∃εOOWn+⊃β←O##?W"β7↔;&K?91π;#πQπ≠#?Wf!β∀hSOSπ&+⊃β/!β;?"βCK?6+⊃β.≠πWO*β'QβO→βββ}∪['?/→1≥≥ε;⊃β>CπQβf+[↔1ε{→β∪/#π'0hS'Mβ⊗+GW'⊗+⊃β≠␈⊃βS#*βS#'v;MβSFQβπ⊗)βCK␈3↔⊃8hP4*SF+K∃βO→β;=ε#↔≠'vKS∃β∞sO←↔∩βS=β&C↔O∃πW↔O&K?;Mbβ?→β≡{WKO*aβO'v≠∃β'"β'L4VcπK∨.ceβ¬εkπSS/⊃β?→ε{C';N{99↓¬##'MεCπ;∪␈+Qβ'~β¬βO/!β?→ε;W'∪.c';↔~βS#π h+∪↔≡≠K'/→β←#∂!β'Mε#↔O'⊗+⊃β'rβ¬βC⊗{?→1ε;⊃β>K[↔Mε9β↔F7C3*βO'7NcπIβ&yβS#(h+#?n+←?KZβCK?⊗c↔7Mph(4*6KKOQbβ¬β≠/9β←?⊗#Mβ?rβ←#π"β∪?↔~βπ;⊃ε#?↔Mεs?QβF[∃β&yβ∃πβK?[.!9↓αN{Uβ∂∞qβπO∨+7∀4V31β&C∃βK.c↔Mβ}1β≠'↔≠Q7?⊗#↔Iβf{∨'
ε;⊃β∂∪'S#n+S'
r↓αS#/→1β'2βg?Uπ;';⊃π+Aβ←O# 4)'A-A/CiKe⊃π≠?7↔>C↔K∃bβg?Uε≠π9βNk7↔∪NS↔3JβK↔∪.≠∃βSFKMβSz↓∪awJ!β←'&C?WQε84+/CC3πvS'?rq↓αC⊗{?≠Mε∪eβ'v#W∂SN{91βF{←↔[/⊃1βK/W'K*β7↔;&K?9β&CπQβ&C'MβO→β←#∂ 4+g␈)βπK*β∪?'v91βπv!βg?*βO#?.c⊃β'&+;S'7IβO↔εKπS.ceβSF)βπ≡)β∂π≡)βπ;"βS#∀hS';∪.≠S'[*βOS↔αq↓α'rβ7?O"β?→β&C∃β∪}kπ';~βS#π"β←∃β∂∪∃β←␈∪/';:aβS#/∪∃βπ⊗)βS←xh+≠3∂3?KMε{→β'v#W∂SN{99↓∧3?Iβ/Cπ7Cf)1β←O#!β3O≠SMβ>)β#π6)βS#*βπc'}kL4)""rC#JBr:&bH⊃ S*rq0⊗dqβT∩eβ#%"d!βU$
bC#%G)%$EA#U:qebC#%G)%%⊃ h+π; h)⊃∩eβ#%"dr&1$"@Sbqg):q2eβ#%#*HFrCFI#bqw)%$EA#U:qebC#%G)%%9" 4*g␈)βO#␈+3⊃βn/∃βO!β∂3.Iβ←FK∂!β6{K5β}1β';'+∂S'}qβg?*βπK∃π+O';:aβπ;"βπ3←∂KL4+N#↔;SN3eβSF)βCK.#'∂π&)↓∩rεC%#UJ!βS#∂!β'Mε∪↔';:βWO↔"p4(4T{≠S↔rβg?Uπ;'31εs↔↔⊃π#=βC⊗{[∃β
βOSπ&+7↔;"βS#π"β'Mβ
βOWπ∪?3.iβ?→π##∃βn'84WβK?f+5βg␈)βπK*β←?K↑K;≥β}q9↓α6{Iβ↔F7C3*aβ'9πβK?f+5↓Es	β?9πβπ∨∃βAe1βN{Uβ7∂H4+;.+⊃βSzβWO∃π##∃β6∂Qβ&CπQ↓'cOπ7.c↔;∨&CroUg2ty#fc↔;∨&Crq3+ks3↔v;S#rbcY%⊃ph*πOZβg?W↔≠↔3→Rβ#?]ε{['␈+Mβ'~βS#'~β≠π∂#y↓α#/∪∃βg␈)β7πJβ∃βnKO3↔"βeβ&C∃β≠∞≠P4+&CπQβ&C∃β≠.s∂S'}qβ'Mεsπ7↔"βsOπn+3↔;?##q1ε∪WQβ&CπQβ&{↔Mβv{Qβ7.9βng≠1β¬πβK'?⊗Jq?xhSS#π"β'Qβ∞≠SWπfceβ∪}+Mβ←FQβ'"β∂3πNkMβSzβ∪=9αα7π;Jβ?S#/⊃β≠Wv≠S'?w_4)#g≠π7↔7∪';∨/a1βs⊗3π;≡+∪q1ε+S
9Jβπ3Ozβ#π[*β;π7/→βS#∂!βOW>;↔OQπ##↔'∩β∂?K⊗+∂S;/≠M84Ph*S#*βOSπ&+7↔;"↓∪sO∞k↔3↔v;S#r←)3ZtrCs3↔v;S#rbcUwsf+;∨SGbq3YJ!1βSF+91βO→βO?n+S#'v84+SFQβ#∂→βS=ε∪∃βC⊗{[↔⊃r↓α;?:βg?Uπ≠#?Wf!β∪↔≡K∪∃βF{]β↔∂≠eβ'"β'Mβ&yβCK␈3∃9↓∧K→β'"β'L4V	β7π'#↔Iβ}1βO'oβ3∃β'∪π;O6{K7π&K?;Mε;⊃β∨+OS/#'?;~β?→β&+K7MαCOW∂BβπM1ε3?H4V+cπ7εc∃1↓'cπCC.s∪rndr&135iwY⊃JβS#↔rβg?Uε≠π9β≡C?]β&C∃βO.∪OS''+S'?rβ'9β}s∀4+fK;∃1ε{I1βN1βg?*βπK∃εK9β¬εCWKKJaβ←KO#∃ββε∪eβSF)β∪↔6K;'SN{9β?2βsπCε+;∪q`h)∩sf#?SO~!9≥≥αα#?←/3↔I1εK9βSF)β∂π≡)β?→π##∃βg≠π7↔f+;∨SGaβ≠Wv≠S'?rβ←∃β>K31βv+↔⊂4VK;∪W∨#'?9π#=βC⊗{[∃βO#Mβ∂␈∪K↔∂&s↔OMr↓αS#/∪↔≠?⊗)1β'"β'Mβv{QβS⊗K['πbaβπ;"βg?ThSO#?.c⊃βOF{]βπfaβS#*βOS↔π→β?→π##∃βNs∪W∂&K?98hP4*7␈≠Qβ?2βWMβ⊗+∨'9π;?K-ε∪eβπ'#π∂/Ns≥βSF)β7πNqβCK}∪3↔5ε#'K↔∨#3eβ∞s⊃βSF+91β>C↔84W##'Mπ∪↔GWO∪↔Mβ
β3↔7n	βS=ε∪∃βC⊗{[↔⊃bβ←∃β.KS#↔∩βCWQεKQβ?61βW;&K1β3∂#↔Iβ␈⊂4+C⊗{[∃βO!βK'>CQβπ>eβπv!βS#.qβ∂?w#';W*β←'SBβS#∃εkπ'9πβK??2q↓α␈#!β?2βS#↔≡(4+7/##?∪~βπK∃εCπK⊃π#=βK.⊃1βF{←↔[/⊃9↓α&CWM1εK→βg␈)β∪=π##∃βπ∪??→ε3'KO"βπMβλh+K?.;!β∪⊗≠Qβ∞s⊃βSF+9βK.≠?CeεKQβ.3?K∃εCπ;∪Ns≥β'"β'91εKQβ'~β↔O"βS=βπ+P4+6KKOQπ##∃βπ∪??≠~β?→β∞c1βSF)β3↔as that you are using, and then the main
proof.  Also, please don't turn in parts of your work that turned out to
be ``dead ends'' in an attempted proof.

As an example of these guidelines, consider problem 4.1 on page 89.  The
statement to be proved is $∀x\,u\,v.\,x\in u∪v⊃x\in u∨x\in v$.  The symbols
``$\in$'' and ``$∪$'' are understood to be the |member| function and the
|union| function which is part of problem 22 on page 47.  Below is a proof
that would be suitable as a homework solution.  The proof is given in a
different typeface to separate it from some comments.

\vskip 10pt
{\parskip 8pt \parindent 0pt
\font\ss=cmss10
\def\proof{\leftskip 0.6truein \rightskip 0.6truein\ss}

{\proof
The |member| function is defined on page 16 as
$$|member|[x,u]←\NOT\N u\AND[[x=\A u]\OR|member|[x,\D u]].$$
By the form of the recursion, this function is known to terminate, so
we may use the fact that
$$∀x\,u.\,x\in u≡¬\N u∧(x=\A u∨x\in\D u).$$
\par}
This implicitly uses a lot of the theory developed in chapter 3, but
that's all right.  If we were not sure that |member| terminated, we would
need the techniques in section 3.7.  The reason for starting with this
property of |member| is that we will later discover it is needed as a
lemma, so it is best to get it out of the way before things get
complicated.
\par
{\proof
For the |union| function, which we abbreviate $∪$, we use the program
$$\eqalign{u∪v←\null&\IF\N u\THEN v\cr
&\ELSE\IF \A u\in v\THEN \D u ∪ v\cr
&\ELSE \A u\.[\D u ∪ v].\cr}$$
Let $\Phi(u)$ be the formula $x\in u∪v⊃x\in u∨x\in v$.
\par}
Here you might choose to say, ``We will prove $∀u.\,\Phi(u)$ by induction,''
but it is already fairly clear what you are trying to do.
\par
{\proof First, $\Phi(\NIL)$
is $x\in\NIL∪v⊃x\in\NIL∨x\in v$.  By the definition of $∪$,
$$\eqalign{\NIL∪v&\null=\IF\N\NIL\THEN v\ELSE\ldots\cr
&\null=v,\cr}$$
so the left side of $\Phi(NIL)$ becomes $x\in v$ and $\Phi(\NIL)$ is true.
\par}
Rather than expanding the $∪$, you might have first tried
using the definition
of $\in$ to simplify one of the formulas.  Since this doesn't work, it is left
out of the final proof.
\par
{\proof Now assume $¬\N u$ and $\Phi(\D u)$, which is
$$x\in\D u∪v⊃x\in\D u∨x\in v.$$
From this we will prove $\Phi(u)$.
\par}
It is often useful to write down $\Phi(\D u)$ at this point, as was done, just
so that you can see exactly what it is that you are assuming.  This may help you
decide how to proceed; in this case we will win if we can get
$x\in\D u∪v$ as part of our formula.
\par
{\proof
$$\baselineskip15pt\lineskip3pt\lineskiplimit3pt
\halign{$\displaystyle{#}$&$\displaystyle{#}$\hfill\cr
⊗⊗\Phi(u)&\null≡x\in u∪v⊃x\in u∨x\in v\cr
&\null≡x\in[\IF\A u\in v\THEN\D u∪v\ELSE\A u\.[\D u∪v]]⊃x\in u∨x\in v\cr
\noalign{\hbox{(using the definition of $∪$ and the assumption $¬\N u$)}}
&\null≡|IF|\,\A u\in v\,|THEN|\,x\in\D u∪v⊃x\in u∨x\in v\cr
\noalign{\nobreak}
&⊗|ELSE|\,x\in\A u\.[\D u∪v]⊃x\in u∨x\in v\cr}$$
If $\A u\in v$, we use the inductive assumption to show $x\in\D u∨x\in v$,
and then the definition of $\in$ (above) to show $x\in u∨x\in v$.
In the other case, given $x\in\A u∪v$, the definition of $\in$ can be
used to show that $x=\A u∨x\in\D u∪v$; from the inductive hypothesis this
implies $x=\A u∨x\in\D u∨x\in v$, and, applying the definition of $\in$ one
more time, this proves $x\in u∨x\in v$.
\par}
A lot of details, but each of the steps above is important to show that you
understand why the proof is working.  Some steps were left out, such as
showing that $\A[\A u\.[\D u∪v]]=\A u$ and $\D[\A u\.[\D u∪v]]=\D u∪v$,
because this is fairly straightforward.
\par
{\proof Therefore, $∀u.\,\Phi(u)$ is true.  Since we made no assumptions
about $x$ or $v$, we can quantify over these also and get
$$∀x\,u\,v.\,x\in u∪v⊃x\in u∨x\in v.$$}
\par
} % end this whole business

\vskip 10pt

Notice that there is a lot of text as well as formulas in the proof.  It
helps your proof's readability immensely if you include statements about
the relation of formulas in the proof to each other, especially when you
are referring to facts proved elsewhere.

\vskip 10pt

On an exam, there isn't enough time for a proof as shown above.  You may
be asked only to recognize that induction is needed and to state the
formula $\Phi(u)$ that is used in the induction (or $\Phi(x)$ in the case
of S-expression induction).

If a full proof is asked for, what is expected is that your solution
includes all the necessary steps (thus in an induction, don't leave out
the base case) and include as many of the details as you have time to
write.  If you omit part of a proof, it may seem like you do not know how
to do that part, and you will then not receive credit for it.  Since you
won't have time to recopy your proofs, be sure to cross out any part that
is wrong or does not lead toward the solution.

\vfill\end